Nuprl Lemma : mu-bound-property+
0,22
postcript
pdf
b
:
,
f
:(
b
). (
n
:
b
.
f
(
n
))
{mu(
f
)
b
&
f
(mu(
f
)) & (
i
:
b
.
i
<mu(
f
)
f
(
i
))}
latex
Definitions
b
,
{
i
..
j
}
,
,
t
T
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
x
:
A
.
B
(
x
)
,
,
A
B
,
A
,
False
,
P
Q
,
{
T
}
Lemmas
mu-bound-property
,
nat
wf
,
bool
wf
,
int
seg
wf
,
assert
wf
,
mu-bound
origin
b:
, f:(b
). (
n:b. f(n)) 
{mu(f) 
b & f(mu(f)) & (i:b. i<mu(f) 
f(i))} b:, f:(b). (n:b. f(n)) {mu(f) b & f(mu(f)) & (i:b. i<mu(f) f(i))} 
b
} Tx:A. B(x)x:A. B(x)
BA Q